Clausola di Horn

In logica, e in particolare nel calcolo proposizionale, una clausola di Horn è una disgiunzione di letterali in cui al massimo uno dei letterali è positivo. Prendono il nome da Alfred Horn che per primo ne evidenziò l'importanza (1951).^[1]

Un esempio di clausola di Horn è il seguente:

${\displaystyle \neg A\vee \neg B\vee C}$

Il numero dei letterali può essere arbitrario (anche zero); la condizione che al massimo uno sia positivo permette di scrivere la clausola sotto forma di implicazione.

Se il numero di letterali positivi è esattamente uno, la clausole di Horn vengono dette "definite", la cui premessa (corpo) è una congiunzione di letterali positivi e la sua conclusione (testa) è un singolo letterale positivo.

Partendo dall'esempio, applichiamo prima De Morgan:

${\displaystyle \neg (A\wedge B)\vee C}$

Dopodiché utilizziamo l'equivalenza logica:

${\displaystyle \neg X\vee Y\equiv X\Rightarrow Y}$

Ricaviamo quindi:

${\displaystyle (A\wedge B)\Rightarrow C}$